IsMonHom{<+>hgrp,<,+>}(n.nat(n)) 

latex

Up	groups 1
Definitions of Statement	|g|, *, e, Mon, AbMon, Group{i}, AbGrp, IsMonHom{M1,M2}(f), OCMon, OGrp, ghgrp, <+>, <,+>, nat(n)
Definitions	t  T, t.2, t.1, x f y, x:A. B(x), e, *, |g|, FunThru2op(A;B;opa;opb;f), P & Q, <,+>, IsMonHom{M1,M2}(f), nat(n), <+>, ghgrp, False, P  Q, A, A  B, ,
Lemmas	int add grp wf2, hgrp of ocgrp wf, grp car wf, int hgrp to nat wf, add nat wf, le wf